\begin{tabbing}
update{-}antecedent\{i:l\}(${\it es}$;${\it Cmd}$;${\it Sys}$;${\it Config}$;$u$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} . ($u$($e$) $<$ $e$))\+
\\[0ex]\& (\=$\forall$$e$:\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} .\+
\\[0ex](\=($\uparrow$(($u$($e$)) $\in_{b}$ ${\it Sys}$))\+
\\[0ex]$\Rightarrow$ (valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$u$($e$)) \& csupdate{-}cmds(${\it Sys}$($e$)) = sys{-}cmds(${\it Sys}$($u$($e$)))))
\-\\[0ex]\& (\=($\uparrow$(($u$($e$)) $\in_{b}$ ${\it Config}$))\+
\\[0ex]$\Rightarrow$ \=(($\uparrow$ccsucc?(${\it Config}$($u$($e$))))\+
\\[0ex]\& ccsucc{-}id(${\it Config}$($u$($e$))) = loc($e$)
\\[0ex]\& let \=$n$\= = ccsucc{-}num(${\it Config}$($u$($e$))) in\+\+
\\[0ex]($n$ $<$ $\parallel$cmd{-}history($u$($e$))$\parallel$)
\-\\[0ex]\& csupdate{-}cmds(${\it Sys}$($e$)) = nth\_tl($n$;cmd{-}history($u$($e$))))))
\-\-\-\-\\[0ex]\& (\=$\forall$$e_{1}$, $e_{2}$:\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} .\+
\\[0ex]($u$($e_{1}$) $<$loc $u$($e_{2}$)) $\Rightarrow$ (loc($e_{1}$) = loc($e_{2}$)) $\Rightarrow$ ($e_{1}$ $<$loc $e_{2}$))
\-\\[0ex]\& (\=$\forall$$e$:\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} , $s$:E.\+
\\[0ex]($s$ $<$loc $u$($e$))
\\[0ex]$\Rightarrow$ \=((($\uparrow$($s$ $\in_{b}$ ${\it Sys}$)) \& valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$s$))\+
\\[0ex]$\vee$ (($\uparrow$($s$ $\in_{b}$ ${\it Config}$)) \& ($\uparrow$ccsucc?(${\it Config}$($s$)))))
\-\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:\{$e$:E(${\it Sys}$)$\mid$ $\uparrow$csupdate?(${\it Sys}$($e$))\} . ($u$(${\it e'}$) = $s$)))
\-\-
\end{tabbing}